\begin{tabbing}
@$i$: $k$ affects only $L$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$@$i$.\+
\\[0ex]kind($e$) $=$ $k$
\\[0ex]$\Rightarrow$ (\=$\forall$$x$:Id.\+
\\[0ex]($\neg$($x$ after $e$) $=$ ($x$ when $e$) $\Rightarrow$ ($x$ $\in$ $L$)) \& ($\neg$($x$ $\in$ $L$) $\Rightarrow$ ($x$ after $e$) $=$ ($x$ when $e$)))
\-\-
\end{tabbing}